Inference at * 1 2 1 
Iof proof for Lemma member-exists:



1. T : Type
2. u : T
3. v : T List
4. x:T. (x  [u / v])
5. [u / v] = []
  False 

latex

 by ((((ApFunToHypEquands `Z' ||Z||  (-1)) 
THENM (Reduce (-1)))) 
TCollapseTHEN (Auto')) 

latex

TC.

Definitions

||as||, , type List